<!DOCTYPE html PUBLIC "-//W3C//DTD XHTML 1.0 Strict//EN"
    "http://www.w3.org/TR/xhtml1/DTD/xhtml1-strict.dtd">

<html xmlns="http://www.w3.org/1999/xhtml" xml:lang="en" lang="en-AU">
  <head>
    <meta http-equiv="content-type" content="application/xhtml+xml; charset=utf-8" />
    <meta name="author" content="Lubos Brim" />
    <meta name="generator" content="GNU Emacs" />
    <link rel="icon" href="pics/divine-ico.png" type="image/x-icon" />
    <link rel="stylesheet" type="text/css" href="divine-screen-alt.css" media="screen, tv, projection" title="Default" />

    <title>Publications</title>
  </head>

  <body>
    <!-- For non-visual user agents: -->
      <div id="top"><a href="#main-copy" class="doNotDisplay doNotPrint">Skip to main content.</a></div>

    <div id="header">
      <div class="superHeader">
        <span>Quick Links:</span>
        <a href="http://www.fi.muni.cz/paradise/" title="ParaDiSe laboratories">PARADISE LABS</a> |
        <a href="divine-cluster.html" title="Divine Cluster pages">DIVINE CLUSTER</a> |
  <a href="divine-mc.html" title="Divine Multi-Core pages">DIVINE MULTI-CORE</a> |
  <a href="divine-cuda.html" title="Divine CUDA pages">DIVINE CUDA</a> |
  DIVINE I-O  <!-- <a href="page.php?page=divine-io" title="Divine External-Memory pages">DIVINE I-O</a>  --> |
        <a href="probdivine.html" title="ProbDivine pages">PROB-DIVINE</a> |
  BIO-DIVINE  <!-- <a href="page.php?page=biodivine" title="BioDivine pages">BIO-DIVINE</a> -->
      </div>

      <div class="midHeader">
          <h1 class="headerTitle">DIVINE</h1>
          <div class="headerSubTitle">Distributed and Parallel Verification Environment</div>

        <br class="doNotDisplay doNotPrint" />
        <div class="headerLinks">
	</div>
      </div>
      <div class="subHeader">
        <span class="doNotDisplay">Navigation:</span>
        <a href="index.html">Main Page</a> |
        <a href="overview.html">DiVinE Overview</a> |
        <a href="language.html">Language Guide</a> |
        <a href="tool.html">Tool Guide</a> |
        <a href="publications.html">Publications</a> |
        <a href="casestudies.html">Experiments</a> |
        Benchmarking  <!-- <a href="page.php?page=benchmark">Benchmarking</a> --> | 
        <a href="http://divine.fi.muni.cz/page.php?page=download">Download</a> |
        <a href="contact.html">Contact us</a>
      </div>
    </div>

    <!-- ##### Main Copy ##### -->
    <div id="main-copy" style="max-width: 1000px">
      <h1>Publications</h1>     <br/><br/><h2 id="y2009">2009</h2><hr>J. Barnat and L. Brim and S. Edelkamp and D. Sulewski and P. Simecek: 
<b>Can Flash Memory Help in Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=453">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/c529e6a52f1dc38ef7e75de970868f45.pdf">pdf</a>]<br/>
<i>Formal Methods for Industrial Critical Systems (FMICS 2008)</i>, Springer-Verlag, 2009, volume 5596 of LNCS, 150--165.
<br/><br/><hr>J. Barnat and J. Chaloupka and J. Van De Pol: 
<b>Distributed Algorithms for SCC Decomposition</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=470">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/28c2bef890f71c76a1c2e2be436a401b.pdf">pdf</a>]<br/>
<i>To appear in Journal of Logic and Computation</i>, volume , 2009, .<br/><br/><hr>K. Verstoep and H. Bal and J. Barnat and L. Brim: 
<b>Efficient Large-Scale Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=467">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/f315f267175558f4d08b8ddc3bb5ee4b.pdf">pdf</a>]<br/>
<i>23rd IEEE International Parallel & Distributed Processing Symposium (IPDPS 2009)</i>, IEEE, 2009.
<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova: 
<b>Local Quantitative LTL Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=452">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/f3efc5a267c4839ffb01dfcc9313ff6f.pdf">pdf</a>]<br/>
<i>Formal Methods for Industrial Critical Systems (FMICS 2008)</i>, Springer-Verlag, 2009, volume 5596 of LNCS, 53--68.
<br/><br/><br/><br/><h2 id="y2008">2008</h2><hr>J. Barnat and L. Brim and P. Rockai: 
<b>DiVinE Multi-Core -- A Parallel LTL Model-Checker</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=451">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/717db36bf78a473cd024b187b0ad199e.pdf">pdf</a>]<br/>
<i>Automated Technology for Verification and Analysis</i>, Springer, 2008, volume 5311 of LNCS, 234-239.
<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and S. Drazan and D. Safranek: 
<b>Parallel Model Checking Large-Scale Genetic Regulatory Networks with DiVinE</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=357">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/d5e5228ea371071347581febc783a133.pdf">pdf</a>]<br/>
<i>ENTCS</i>, volume 194(3), 2008, 35--50.<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova: 
<b>ProbDiVinE-MC: Multi-core LTL Model Checker for Probabilistic Systems</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=464">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/3cb1d70a596cc338389462615d260e5e.pdf">pdf</a>]<br/>
<i>QEST '08: Proceedings of the 2008 Fifth International Conference on Quantitative Evaluation of Systems</i>, IEEE Computer Society, 2008, 77--78.
<br/><br/><hr>J. Barnat and L. Brim and P. Simecek and M. Weber: 
<b>Revisiting Resistance Speeds Up I/O-Efficient LTL Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=426">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/c0bd0d0730a23eedb18cdb478ec0622e.pdf">pdf</a>]<br/>
<i>Tools and Algorithms for the Construction and Analysis of Systems (TACAS).</i>, Springer, 2008, volume 4963 of LNCS, 48-62.
<br/><br/><hr>J. Barnat and P. Rockai: 
<b>Shared Hash Tables in Parallel Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=331">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/168699cd5787307ee3c8c1a509327e6f.pdf">pdf</a>]<br/>
<i>ENTCS</i>, volume 198(1), 2008, 79--91.<br/><br/><hr>L. Brim and J.Barnat: 
<b>Squeeze All the Power Out of Your Hardware to Verify Your Software!</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=454">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/1b8e5b93c422a196a1a24f4f29574325.pdf">pdf</a>]<br/>
<i>ISOLA 2008</i>, Springer Verlag, 2008, volume 17 of CCIS, 604-618.
<br/><br/><br/><br/><h2 id="y2007">2007</h2><hr>J. Barnat and L. Brim and P. Simecek: 
<b>I/O Efficient Accepting Cycle Detection</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=276">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/13c3a64c56afe0f2ed4f8f065f9ccbd6.pdf">pdf</a>]<br/>
<i>Computer Aided Verification</i>, Springer, 2007, volume 4590 of LNCS, 281--293.
<br/><br/><hr>Jiri Barnat and Lubos Brim and Martin Leucker: 
<b>Parallel Model Checking  and the FMICS-jETI Platform</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=344">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/6dc2d84c611041f04b21be80f096b449.pdf">pdf</a>]<br/>
<i>The Twelfth IEEE International Conference on Engineering of Complex Computer Systems (ICECCS 2007)</i>, IEEE Computer Society Press, 2007.
<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and S. Drazan and D.Safranek: 
<b>Parallel Model-Checking Genetic Regulatory Networks</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=379">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/f8b7a701fce4c1f61cfa0c3520219788.pdf">pdf</a>]<br/>
<i>Towards Systems Biology</i>, Verimag, 2007.
<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and M. Ceska and J. Tumova: 
<b>ProbDiVinE: A Parallel Qualitative LTL Model Checker</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=330">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/f8d3829faab2a2ba0da7f76b381a84f3.pdf">pdf</a>]<br/>
<i>Fourth International Conference on the Quantitative Evaluation of Systems (QEST'07)</i>, IEEE Computer Society, 2007, 215-216.
<br/><br/><hr>J. Barnat and L. Brim and P. Rockai: 
<b>Scalable Multi-core LTL Model-Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=297">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/bd4df1ce0205b57753ace9e3d208b618.pdf">pdf</a>]<br/>
<i>Model Checking Software</i>, Springer, 2007, volume 4595 of LNCS, 187--203.
<br/><br/><hr>L. Brim and J. Barnat: 
<b>Tutorial: Parallel Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=347">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/e1db95c0c4bda337d48b9471eab9dffd.pdf">pdf</a>]<br/>
<i>Model Checking Software</i>, Springer, 2007, volume 4595 of LNCS, 2--3.
<br/><br/><br/><br/><h2 id="y2006">2006</h2><hr>Jiri Barnat and Ivana Cerna: 
<b>Distributed Breadth-First Search LTL Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=252">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/c4b346c09fac280aff9d19ca64b36ad6.pdf">pdf</a>]<br/>
<i>Special Issue on Parallel and Distributed Databases of Formal Methods in System Design</i>, volume 29(2), September 2006, 117-134(18).<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and P. Moravec and P. Rockai and P. Simecek: 
<b>DiVinE -- A Tool for Distributed Verification (Tool Paper)</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=254">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/367fe9626b143c6b60adc4da816a3d17.pdf">pdf</a>]<br/>
<i>Computer Aided Verification</i>, Springer Berlin / Heidelberg, 2006, volume 4144/2006 of LNCS, 278-281.
<br/><br/><hr>Jiri Barnat and Pavel Moravec: 
<b>Parallel Algorithms for Finding SCCs in Implicitly Given Graphs</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=257">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/e974c177c7be16c6fdc03950b2ac9221.pdf">pdf</a>]<br/>
<i>Formal Methods: Applications and Technology</i>, Springer, 2006, volume 4346 of LNCS, 316--330.
<br/><br/><br/><br/><h2 id="y2005">2005</h2><hr>J. Barnat and L. Brim and I. Cerna: 
<b>Cluster-Based LTL Model Checking of Large Systems</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=253">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/037a979ec83f60850242fd7f7364c162.pdf">pdf</a>]<br/>
<i>Formal Methods for Components and Objects</i>, 2005, LNCS, 259-279.
<br/><br/><hr>J. Barnat and L. Brim and I. Cerna and P. Simecek: 
<b>DiVinE -- The Distributed Verification Environment</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=255">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/f883df687d626a8b581e1a7d4504a972.pdf">pdf</a>]<br/>
<i>Proceedings of 4th International Workshop on Parallel and Distributed 
Methods in verifiCation</i>, 2005, 89--94.
<br/><br/><hr>J. Barnat and V. Forejt and M. Leucker and M. Weber: 
<b>DivSPIN -- A SPIN compatible distributed model checker</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=256">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/95d57a354d83786ee3621582ebd5a7b0.pdf">pdf</a>]<br/>
<i>Proceedings of 4th International Workshop on Parallel and Distributed 
Methods in verifiCation</i>, 2005, 95--100.
<br/><br/><hr>J. Barnat and L. Brim and J. Chaloupka: 
<b>From Distributed Memory Cycle Detection to Parallel LTL Model
  Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=190">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/530ea1c34d68b7b98681ec81fa0bd1ee.pdf">pdf</a>]<br/>
<i>Electronic Notes in Theoretical Computer Science</i>, volume 133(1,
    month), 2005, 21--39.<br/><br/><hr>L. Brim and I. Cerna and P. Moravec and J. Simsa: 
<b>How to Order Vertices for Distributed LTL Model-Checking Based on Accepting Predecessors</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=211">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/1c31f9265b4fa2fb40bc623096bce1c6.pdf">pdf</a>]<br/>
<i>4rd International Workshop on Parallel and Distributed Methods in verifiCation</i>, 2005.
<br/><br/><br/><br/><h2 id="y2004">2004</h2><hr>L. Brim and I. Cerna and P. Moravec
                            and J. Simsa: 
<b>Accepting Predecessors are Better than Back 
                    Edges in Distributed LTL Model-Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=194">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/9bec21e5e2fe9bca8158195a71f0a3f8.pdf">pdf</a>]<br/>
<i>5th International Conference on Formal Methods in Computer-Aided Design (FMCAD'04)</i>, Springer-Verlag, 2004, volume 3312 of LNCS, 352-366.
<br/><br/><hr>Jiri Barnat: 
<b>Distributed Memory LTL Model Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=191">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/74925f5d8351a5a41120c11f26f3a21b.pdf">pdf</a>]<br/>
Ph.D. Thesis, <i>Masaryk University Brno, Faculty of Informatics</i>, 2004.
<br/><br/><hr>Lubos Brim and
               Ivana Cerna and
               Lukas Hejtmanek: 
<b>Distributed Negative Cycle Detection Algorithms</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=457">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/67e719c06140dbdc9db4eabbd2f6eb2e.pdf">pdf</a>]<br/>
<i>Parallel Computing: Software Technology, Algorithms, and Applications (PARCO'03)</i>, Elsevier, 2004, volume 13 of Advances in Parallel Computing, 297--304.
<br/><br/><hr>L. Brim and I. Cerna and P. Moravec and J. Simsa: 
<b>Distributed Partial Order Reduction of State Spaces</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=179">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/3509684f5615a6cc070ff1fae1922f11.pdf">pdf</a>]<br/>
<i>3rd International Workshop on Parallel and Distributed Methods in verifiCation</i>, 2004.
<br/><br/><br/><br/><h2 id="y2003">2003</h2><hr>I. Cerna and R. Pelanek: 
<b>Distributed Explicit Fair Cycle Detection</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=86">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/0b12de9f069f5641c323d1602e3ba2a4.pdf">pdf</a>]<br/>
<i>Proc.  SPIN workshop</i>, Springer, 2003, volume 2648 of LNCS, 49-74.
<br/><br/><hr>L. Brim and J. Barnat: 
<b>Distribution of Explicit-State LTL
Model-Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=151">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/dbc74a076cf9ff95a9e7b544820a1daa.pdf">pdf</a>]<br/>
<i>8th International Workshop on Formal Methods for Industrial Critical Systems (FMICS 03)</i>, Elsevier, 2003, volume 80 of Electronic Notes in Theoretical Computer Science.
<br/><br/><hr>J. Barnat and L. Brim and J. Chaloupka: 
<b>Parallel Breadth-First Search LTL
Model-Checking</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=119">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/c774e34946eb387373d317570c86f871.pdf">pdf</a>]<br/>
<i>18th IEEE International Conference on Automated Software
Engineering (ASE'03)</i>, IEEE Computer Society, 2003, 106--115.
<br/><br/><br/><br/><h2 id="y2002">2002</h2><hr>J. Barnat and L. Brim and I. Cerna: 
<b>Property driven distribution of Nested DFS</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=34">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/5f773c95a13c7b85f303123b36985210.pdf">pdf</a>]<br/>
<i>Proc. Workshop on Verification and Computational Logic</i>, 2002, DSSE Technical Report, 1 - 10.
<br/><br/><br/><br/><h2 id="y2001">2001</h2><hr>L. Brim and I. Cerna and  P. Krcal 
             and R. Pelanek: 
<b>Distributed LTL Model Checking Based on Negative 
             Cycle Detection</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=28">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/bc75588e5d9f58e9768ad4bcc15c0791.pdf">pdf</a>]<br/>
<i>Proc. Foundations of Software Technology and Theoretical
               Computer Science</i>, Springer, 2001, 
 opteditor, volume 2245, 
 series of , 96--107.
<br/><br/><hr>J. Barnat and L. Brim and J.
                 Stribrna: 
<b>Distributed LTL Model-Checking 
                 in SPIN</b> [<a href="http://anna.fi.muni.cz/papers/export.cgi?aid=32">bibtex</a>, <a href="http://anna.fi.muni.cz/papers/src/public/8e583540bbfaef57032bb33e14e2c733.pdf">pdf</a>]<br/>
<i>Proc. SPIN Workshop on Model Checking of Software</i>, Springer, 2001, volume 2057 of LNCS, 200 - 216.
<br/><br/></div>

    <!-- ##### Footer ##### -->
    <div id="footer">
<span>Copyright &copy; 2002-2008 ParaDiSe Labs, Faculty of Informatics, Masaryk
University, Brno, Czech Republic</span><br />
      <strong>Updated &raquo;</strong>Wednesday, 3-Sep-2008 16:40 CEST<br />
    </div>
  </body>
</html>


















